structure Compile : COMPILE =
struct
  exception localFail
 
  val compName = "plcc "
  val compilerInfo = String.concat [compName, ": a proof-directed certifying compiler for PointerC"]
  val compilerVersion = String.concat [compName, "version 1.6 (built on May 16 19:30:30 2007)"]
  val copyright = "Copyright (C) Software Security Laboratory, CSD, USTC. 2005-\n\
                  \All rights reserved.\n\
                  \plcc is now developed by the LSS project at this URL: \n\
                  \<http://ssg.ustcsz.edu.cn/lss>\n\
                  \Please consult this URL for more information."
  val usage = "Usage: plcc [options...] file.{c|s|C|S}"
  val forMore = "For more help, try -help or -version."
  
  val options = 
      [("-v", 			"show compiler version information"),
       ("-S",			"output x86 assembly file, not executables"),
       ("-verbose", 		"show compliation process"),
       ("-keep {a|i|c|s|m|x}",  "keep the corresponding intermediate form"),
       ("-output <file>", 	"set the output file name"),
       ("-skipSsa",             "do not conversion to SSA form"),
       ("-noSsaOpt", 		"do not do optimizations on SSA"),
       ("-noRa",                "do not do register allocation optimization"),
       ("-optInfo", 		"show the optimizaton process on SSA form")
       (*("-srcprf", 		"show the process of source-level pointer logic proof"),*)
       (*("-asmprf", 		"show the process of assembly-level pointer proof checking"),*)
       (*("-nocoq",		"do not prove in Coq")*)]
      
  fun say s = print s
  fun sayLn s = print (String.concat [s, "\n"])

  val sayUnknownOption = fn x => sayLn (String.concat ["unknown option : ", x])

  val sayUnknownFile = fn x => sayLn (String.concat ["unknown file : ", File.nameToString x])

  fun getMaxWidth m =
      let fun doit (l, n) =
              case l
               of [] => n
                | (head, _) :: xs =>
                  let val size = String.size head
                  in  if size > n
                      then doit (xs, size)
                      else doit (xs, n)
                  end
      in  doit (m, 0)
      end
      
  val width = getMaxWidth options
	      
  fun spaces n =
      if n < 0
      then raise Fail "compiler bug"
      else let fun doit n =
                   case n
                    of 0 => ""
                     | n => String.concat [" ", doit (n - 1)]
           in  doit n
           end
        
  fun length s = String.size s
  
  fun sayOptions () =
      let fun newSay (s1, s2) =
              print (String.concat [spaces 3,
                                    s1,
                                    spaces (width - length s1 + 1),
                                    s2,
                                    "\n"])
      in  List.app newSay options
      end
      
  fun hasOption (opt, strList) = List.exists (fn x => x = opt) strList
				 
  (* ugly for now, but workable *)
  fun setOptions strList =
      case strList
       of [] => ()
        | x :: xs => 
          case x
           of "-v" => (Control.doShowVersion := true; sayLn compilerVersion; setOptions xs)
            | "-S" => (Control.doKeepAssembly := true; setOptions xs)
            | "-verbose" => (Control.doShowPass := true; setOptions xs)
	    | "-output" =>
	      (case xs
	        of [] =>
	           let val _ = sayLn "no output file name"
		       val _ = sayLn usage
		   in  raise localFail
		   end
		 | y :: ys =>
		   let val _ = Control.doSetFileName := true
		       val _ = Control.fileName := y
		   in  setOptions ys
		   end)
            | "-keep" =>
              (case xs
	        of [] =>
	           let val _ = sayLn "no keep file name"
		       val _ = sayLn usage
		   in  raise localFail
		   end
		 | "a" :: ys =>
		   let val _ = Control.doKeepAst := true
		   in  setOptions ys
		   end
		 | "i" :: ys =>
		   let val _ = Control.doKeepIr := true
		   in  setOptions ys
		   end
		 | "c" :: ys =>
		   let val _ = Control.doKeepCfg := true
		   in  setOptions ys
		   end
		 | "s" :: ys =>
		   let val _ = Control.doKeepSsa := true
		   in  setOptions ys
		   end
		 | "m" :: ys =>
		   let val _ = Control.doKeepMachine := true
		   in  setOptions ys
		   end
		 | "x" :: ys =>
		   let val _ = Control.doKeepAsm := true
		   in  setOptions ys
		   end
		 | _ :: ys =>
		   let val _ = sayLn "unknow options"
		       val _ = sayLn usage
		   in  raise localFail
		   end)
            | "-id" => (Control.doShowIdNums := true; setOptions xs)
            | "-skipSsa" => (Control.doToSsa := false; setOptions xs)
            | "-noSsaOpt" => (Control.doSsaOpt := false; setOptions xs)
            | "-noRa" => (Control.doRaOpt := false; setOptions xs)
            | "-optInfo" => (Control.doShowOptVerbose := true; setOptions xs)
            | _ => (sayUnknownOption x; sayOptions (); raise localFail)
		   
  datatype fileStatus
    = Valid
    | Invalid
      
  fun testFile s =
      case List.rev (String.explode (File.nameToString s))
       of (#"c") :: (#".") :: _ => Valid
        | (#"C") :: (#".") :: _ => Valid
        | (#"s") :: (#".") :: _ => Valid
        | (#"S") :: (#".") :: _ => Valid
        | _ => Invalid
        
  fun callMain file =
      let val _ = if (File.exists file)
                  then ()
                  else 
                   (sayUnknownFile file
		      ; sayOptions ()
		      ; raise localFail)
      in  case testFile file
            of Valid => ((Main.main file) handle Failed => raise localFail)
             | Invalid => (sayLn (String.concat ["invalid file suffix: ", File.nameToString file])
                         ; sayOptions ()
                         ; raise localFail)
      end

  fun handleOneArg x =
      case x
       of "-help" => (sayLn usage; sayOptions ())
        | "-version" => (sayLn compilerInfo; sayLn compilerVersion; sayLn copyright)
        | _ => ignore (callMain (File.creat x))
      
  fun compile (name, args) =
      case args
       of [] => (sayLn compilerInfo; sayLn usage; sayLn forMore)
        | [x] => handleOneArg x
        | _ =>  let val revArgs = rev args
                in  setOptions (rev (tl revArgs))
                  ; let val fname = hd revArgs
                    in  ignore (callMain (File.creat fname))
                    end
                end
  
  fun top () =
      (compile (CommandLine.name (), CommandLine.arguments ()))
      handle localFail => ()
end
